the_es:event_system{i:l}. wellfounded{i:l}(es-E(the_es); x,y.es-locl(the_es; x; y)) 

latex

Definitions	event_system{i:l}, P  Q, x,y. t(x;y), P  Q, es-locl(es; e; e'), es-E(es), x:A. B(x), t  T
Lemmas	es-E wf, es-locl wf, strongwf-implies, es-axioms, event system wf